Problem:
 f(0()) -> s(0())
 f(s(x)) -> g(s(s(x)))
 g(0()) -> s(0())
 g(s(0())) -> s(0())
 g(s(s(x))) -> f(x)

Proof:
 Bounds Processor:
  bound: 2
  enrichment: match
  automaton:
   final states: {4,3}
   transitions:
    f1(27) -> 28*
    f1(21) -> 22*
    s1(5) -> 6*
    s1(17) -> 18*
    s1(14) -> 15*
    s1(13) -> 14*
    01() -> 5*
    g1(15) -> 16*
    f2(31) -> 32*
    f2(33) -> 34*
    f0(2) -> 3*
    f0(1) -> 3*
    00() -> 1*
    s0(2) -> 2*
    s0(1) -> 2*
    g0(2) -> 4*
    g0(1) -> 4*
    1 -> 27,17
    2 -> 21,13
    6 -> 32,16,22,28,4,3
    13 -> 33*
    16 -> 34,22,4,3
    17 -> 31*
    18 -> 14*
    22 -> 4*
    28 -> 4*
    32 -> 16,3
    34 -> 16,3
  problem:
   
  Qed